\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{listings}
\usepackage{oz, amsfonts}

\title{Software Engineering\\Assignment 3}
\author{Adrian.Nembach@uni-konstanz.de 01/842319\\Udo.3.Schlegel@uni-konstanz.de 01/840835\\Sirui.Liu@uni-konstanz.de 01/857316}
\begin{document}
\maketitle

\section*{Aufgabe 3.1}
$\{(\forall i)(1 \leq i \leq length \wedge IMPL[i] \neq x)$\\
\begin{itemize}
\item[operation] $INSERT(IMPL: in\ int\_arr; length: in\ int;\ x: in\ int; $\\
$new\_IMPL: out\ int\_arr; new\_length: out\ int)$
\end{itemize}
$(\exists i)((1\leq i \leq new\_length \wedge new\_IMPL[i] = x) $\\
$\wedge (\forall i)((1 \leq i \leq new\_length) \wedge new\_IMPL[i] \neq x) $\\
$\Rightarrow (\exists j)((1 \leq j \leq length) \wedge new\_IMPL[i] = IMPL[j]))$\\
\\
Correctness Argument (informal scetch):\\
\begin{enumerate}
\item The Precondition ensures INV (no element in set is equal to x)
\item Postcondition: There exists an Element that is equal to x in the new set (the inserted one), and for all elements in the new set that are not equal to x there are korrespondence elements in the old set.
\end{enumerate}
\section*{Aufgabe 3.2}
\begin{schema}{Members}
member : \pset NAME\\
birthday : \pset BIRTHDAY\\
gender : \{FERMALE, MALE\} \\
religion : \pset COUNTRIES\\
email : \pset EMAIL\\
premium : \pset \{YES,NO\}\\
\end{schema}
\begin{schema}{ALBUM}
artist : \pset ARTIST\\
 title : \pset TITLE\\
release : \pset RELEASE\\
type : \{CD, LP, Tape, etc.\}, \\
label : \pset  COMPANY\\
 genre: \pset GENRE \\
 track : \pset TRACK \\
cover:\pset COVER \\
reviews : \pset REVIEWS\\
\ST
|reviews| \geq 1\\
\end{schema}
\begin{schema}{AddOrder}
\bigtriangleup MusicStore\\
member? : NAME\\
order? : ALBUM\\
\ST
\forall (m, a) \in orders. (m, a) {\not\in} owns\\
orders' = orders\cup \{member?\mapsto order?\}\\
\end{schema}
\begin{schema}{DownloadAlbum}
\bigtriangleup MusicStore\\
download? : ALBUM\\
member? : NAME
\ST
(\forall m \in member? \cap \forall a \in download?). (m, a) \in orders\\
orders' = orders \setminus \{member? \mapsto download?\}\\
\end{schema}
\begin{schema}{CheckDownload}
member? : NAME\\
owns! : \pset (NAME\times ALBUM)\\
\ST
owns! = \{n \in {\bf ran}\mbox{ }owns | {\bf dom}\mbox{ }owns = member?\}
\end{schema}
\end{document}